Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Making sure tactic errors respect error range bound #3687

Merged
merged 4 commits into from
Jan 18, 2025

Conversation

mtzguido
Copy link
Member

Mostly for Pulse

This is useful for primitives that cannot possibly fail, and have no
effect, but need to be in TAC due to reading some part of the
proofstate. For example, the state of the current error range bound.
When a tactic fails, it raises an exception, which does not read the
current error bound. The interpreter module running the tactic will then
bound the range by reading the current error bound, but it is too late
as it could have been popped away.

This moves the bounding logic into the `fail`s in the tactic module, to
read the bound immediately before raising the exception.

This is mostly useful for Pulse, as there is no way for normal userspace
clients to set the bound, so it wouldn't make a difference. Hence I'm
unsure about this patch.
@mtzguido mtzguido enabled auto-merge January 18, 2025 08:29
@mtzguido mtzguido changed the title Allowing tactics to bound error ranges Making sure tactic errors respect error range bound Jan 18, 2025
@mtzguido mtzguido merged commit c635fa9 into FStarLang:master Jan 18, 2025
10 checks passed
@mtzguido mtzguido deleted the ranges branch January 18, 2025 09:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant